IdrisDoc: [builtins]

[builtins]

data (=) : (x : A) -> (y : B) -> Type

The propositional equality type. A proof that x = y.

To use such a proof, pattern-match on it, and the two equal things will then need to be the same pattern.

Note: Idris's equality type is potentially heterogeneous, which means that it is possible to state equalities between values of potentially different types. However, Idris will attempt the homogeneous case unless it fails to typecheck.

You may need to use (~=~) to explicitly request heterogeneous equality.

A

the type of the left side of the equality

B

the type of the right side of the equality

Refl : x = x

A proof that x in fact equals x. To construct this, you must have already shown that both sides are in fact equal.

A

the type at which the equality is proven

x

the element shown to be equal to itself.

CData : Type
data DelayReason : Type

Two types of delayed computation: that arising from lazy functions, and that
arising from infinite data. They differ in their totality condition.

Infinite : DelayReason
LazyValue : DelayReason
data Delayed : DelayReason -> Type -> Type

The underlying implementation of Lazy and Inf.

Delay : (val : a) -> Delayed t a

A delayed computation.

Delay is inserted automatically by the elaborator where necessary.

Note that compiled code gives Delay special semantics.

t

whether this is laziness from an infinite structure or lazy evaluation

a

the type of the eventual value

val

a computation that will produce a value

record FFI 

An FFI specifier, which describes how a particular compiler
backend handles foreign function calls.

MkFFI : (ffi_types : Type -> Type) -> (ffi_fn : Type) -> (ffi_data : Type) -> FFI
ffi_types

A family describing which types are available in the FFI

ffi_fn

The type used to specify the names of foreign functions in this FFI

ffi_data

How this FFI describes exported datatypes

ffi_types : (rec : FFI) -> Type -> Type

A family describing which types are available in the FFI

ffi_fn : (rec : FFI) -> Type

The type used to specify the names of foreign functions in this FFI

ffi_data : (rec : FFI) -> Type

How this FFI describes exported datatypes

FFI_JS : FFI

The JavaScript FFI. The strings naming functions in this API are
JavaScript code snippets, into which the arguments are substituted
for the placeholders %0, %1, etc.

data FTy : FFI -> List Type -> Type -> Type
FRet : ffi_types f t -> FTy f xs (IO' f t)
FFun : ffi_types f s -> FTy f (s :: xs) t -> FTy f xs (s -> t)
Force : Delayed t a -> a

Compute a value from a delayed computation.

Inserted by the elaborator where necessary.

ForeignPrimType : (xs : List Type) -> FEnv ffi xs -> Type -> Type
IO : (res : Type) -> Type

Interactive programs, describing I/O actions and returning a value.

res

The result type of the program

data IO' : (lang : FFI) -> Type -> Type

The IO type, parameterised over the FFI that is available within
it.

MkIO : (World -> PrimIO (WorldRes a)) -> IO' lang a
Inf : Type -> Type

Possibly infinite data.
A value which may be infinite is accepted by the totality checker if
it appears under a data constructor. At run time, the delayed value will
only be computed when required by a case split.

data JS_FnTypes : Type -> Type
JS_Fn : JS_Types s -> JS_FnTypes t -> JS_FnTypes (s -> t)
JS_FnIO : JS_Types t -> JS_FnTypes (IO' l t)
JS_FnBase : JS_Types t -> JS_FnTypes t
JS_IO : Type -> Type
data JS_IntTypes : Type -> Type
JS_IntChar : JS_IntTypes Char
JS_IntNative : JS_IntTypes Int
data JS_Types : Type -> Type
JS_Str : JS_Types String
JS_Float : JS_Types Double
JS_Ptr : JS_Types Ptr
JS_Unit : JS_Types ()
JS_FnT : JS_FnTypes a -> JS_Types (JsFn a)
JS_IntT : JS_IntTypes i -> JS_Types i
data JsFn : Type -> Type
MkJsFn : (x : t) -> JsFn t
Lazy : Type -> Type

Lazily evaluated values.
At run time, the delayed value will only be computed when required by
a case split.

ManagedPtr : Type
MkFFI : (ffi_types : Type -> Type) -> (ffi_fn : Type) -> (ffi_data : Type) -> FFI
ffi_types

A family describing which types are available in the FFI

ffi_fn

The type used to specify the names of foreign functions in this FFI

ffi_data

How this FFI describes exported datatypes

PE_(a, b) implementation of Decidable.Equality.DecEq_75bec382 : DecEq (Int, Int)
PE_(a, b), Raw implementation of Language.Reflection.Quotable_4799f661 : Quotable (List CtorArg, Raw) Raw
PE_(a, b), Raw implementation of Language.Reflection.Quotable_4e00078a : Quotable (TTName, List CtorArg, Raw) Raw
PE_(a, b), TT implementation of Language.Reflection.Quotable_4799f661 : Quotable (List CtorArg, Raw) TT
PE_(a, b), TT implementation of Language.Reflection.Quotable_4e00078a : Quotable (TTName, List CtorArg, Raw) TT
PE_*_40cb6e4b : Integer -> Integer -> Integer
PE_*_6b31ad5c : Nat -> Nat -> Nat
PE_*_7200248c : Double -> Double -> Double
PE_*_ba2f651f : Int -> Int -> Int
PE_+_40cb6e4b : Integer -> Integer -> Integer
PE_+_6b31ad5c : Nat -> Nat -> Nat
PE_+_7200248c : Double -> Double -> Double
PE_+_ba2f651f : Int -> Int -> Int
PE_-_40cb6e4b : Integer -> Integer -> Integer
PE_-_7200248c : Double -> Double -> Double
PE_-_ba2f651f : Int -> Int -> Int
PE_/=_32c264fb : Bool -> Bool -> Bool
PE_/=_ba2f651f : Int -> Int -> Bool
PE_/_7200248c : Double -> Double -> Double
PE_<$>_2ddfe5d0 : (func : a -> b) -> IO' (MkFFI C_Types String String) a -> IO' (MkFFI C_Types String String) b
PE_<$>_d4eefcf3 : (func : a -> b) -> Elab a -> Elab b
PE_<=_22f242c8 : Char -> Char -> Bool
PE_<=_40cb6e4b : Integer -> Integer -> Bool
PE_<=_6b31ad5c : Nat -> Nat -> Bool
PE_<=_ba2f651f : Int -> Int -> Bool
PE_<_1676ea41 : Prec -> Prec -> Bool
PE_<_22f242c8 : Char -> Char -> Bool
PE_<_32c264fb : Bool -> Bool -> Bool
PE_<_40cb6e4b : Integer -> Integer -> Bool
PE_<_6b31ad5c : Nat -> Nat -> Bool
PE_<_7200248c : Double -> Double -> Bool
PE_<_9b1b58ef : () -> () -> Bool
PE_<_a2d818a2 : Fin n -> Fin n -> Bool
PE_<_ba2f651f : Int -> Int -> Bool
PE_<_c1eaf49 : String -> String -> Bool
PE_<_d5e44cdf : Bits16 -> Bits16 -> Bool
PE_<_d6064c5d : Bits32 -> Bits32 -> Bool
PE_<_d63daea2 : Bits64 -> Bits64 -> Bool
PE_<_e41bdaf : Bits8 -> Bits8 -> Bool
PE_==_1676ea41 : Prec -> Prec -> Bool
PE_==_22f242c8 : Char -> Char -> Bool
PE_==_32c264fb : Bool -> Bool -> Bool
PE_==_346eb07c : Ordering -> Ordering -> Bool
PE_==_40cb6e4b : Integer -> Integer -> Bool
PE_==_5a6178be : ManagedPtr -> ManagedPtr -> Bool
PE_==_6b31ad5c : Nat -> Nat -> Bool
PE_==_7200248c : Double -> Double -> Bool
PE_==_9b1b58ef : () -> () -> Bool
PE_==_a2d818a2 : Fin n -> Fin n -> Bool
PE_==_ba2f651f : Int -> Int -> Bool
PE_==_c1eaf49 : String -> String -> Bool
PE_==_caeefbca : Ptr -> Ptr -> Bool
PE_==_d5e44cdf : Bits16 -> Bits16 -> Bool
PE_==_d6064c5d : Bits32 -> Bits32 -> Bool
PE_==_d63daea2 : Bits64 -> Bits64 -> Bool
PE_==_e41bdaf : Bits8 -> Bits8 -> Bool
PE_>=_1676ea41 : Prec -> Prec -> Bool
PE_>=_22f242c8 : Char -> Char -> Bool
PE_>=_40cb6e4b : Integer -> Integer -> Bool
PE_>=_ba2f651f : Int -> Int -> Bool
PE_>_1676ea41 : Prec -> Prec -> Bool
PE_>_22f242c8 : Char -> Char -> Bool
PE_>_32c264fb : Bool -> Bool -> Bool
PE_>_40cb6e4b : Integer -> Integer -> Bool
PE_>_6b31ad5c : Nat -> Nat -> Bool
PE_>_7200248c : Double -> Double -> Bool
PE_>_9b1b58ef : () -> () -> Bool
PE_>_a2d818a2 : Fin n -> Fin n -> Bool
PE_>_ba2f651f : Int -> Int -> Bool
PE_>_c1eaf49 : String -> String -> Bool
PE_>_d5e44cdf : Bits16 -> Bits16 -> Bool
PE_>_d6064c5d : Bits32 -> Bits32 -> Bool
PE_>_d63daea2 : Bits64 -> Bits64 -> Bool
PE_>_e41bdaf : Bits8 -> Bits8 -> Bool
PE_Decidable.Equality.(a, b) implementation of Decidable.Equality.DecEq, method decEq_e07dba86 : (x1 : (Int, Int)) -> (x2 : (Int, Int)) -> Dec (x1 = x2)
PE_Decidable.Equality.List a implementation of Decidable.Equality.DecEq, method decEq_c1eaf49 : (x1 : List String) -> (x2 : List String) -> Dec (x1 = x2)
PE_Language.Reflection.(a, b), Raw implementation of Language.Reflection.Quotable, method quote_42a8fa14 : (List CtorArg, Raw) -> Raw
PE_Language.Reflection.(a, b), Raw implementation of Language.Reflection.Quotable, method quote_9fb2a838 : (TTName, List CtorArg, Raw) -> Raw
PE_Language.Reflection.(a, b), Raw implementation of Language.Reflection.Quotable, method quotedTy_1c1cafc1 : Raw
PE_Language.Reflection.(a, b), Raw implementation of Language.Reflection.Quotable, method quotedTy_4f9883b0 : Raw
PE_Language.Reflection.(a, b), TT implementation of Language.Reflection.Quotable, method quote_42a8fa14 : (List CtorArg, Raw) -> TT
PE_Language.Reflection.(a, b), TT implementation of Language.Reflection.Quotable, method quote_9fb2a838 : (TTName, List CtorArg, Raw) -> TT
PE_Language.Reflection.(a, b), TT implementation of Language.Reflection.Quotable, method quotedTy_1c1cafc1 : TT
PE_Language.Reflection.(a, b), TT implementation of Language.Reflection.Quotable, method quotedTy_4f9883b0 : TT
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quote_21164daa : List FunArg -> Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quote_81ff5c9 : List String -> Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quote_9bccd82b : List (TTName, List CtorArg, Raw) -> Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quote_a91ea646 : List ConstructorDefn -> Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quote_b5ff547f : List CtorArg -> Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quote_c5256c59 : List ErrorReportPart -> Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quote_e456e031 : List TyConArg -> Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quotedTy_1507bcbc : Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quotedTy_20086ef3 : Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quotedTy_33ab986c : Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quotedTy_7915b8f7 : Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quotedTy_d09dc8b8 : Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quotedTy_df2fadf0 : Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quotedTy_fc2e868 : Raw
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quote_21164daa : List FunArg -> TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quote_81ff5c9 : List String -> TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quote_9bccd82b : List (TTName, List CtorArg, Raw) -> TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quote_a91ea646 : List ConstructorDefn -> TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quote_b5ff547f : List CtorArg -> TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quote_c5256c59 : List ErrorReportPart -> TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quote_e456e031 : List TyConArg -> TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quotedTy_1507bcbc : TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quotedTy_20086ef3 : TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quotedTy_33ab986c : TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quotedTy_7915b8f7 : TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quotedTy_d09dc8b8 : TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quotedTy_df2fadf0 : TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quotedTy_fc2e868 : TT
PE_List a implementation of Decidable.Equality.DecEq_fc2e868 : DecEq (List String)
PE_List a, Raw implementation of Language.Reflection.Quotable_1507bcbc : Quotable (List CtorArg) Raw
PE_List a, Raw implementation of Language.Reflection.Quotable_20086ef3 : Quotable (List FunArg) Raw
PE_List a, Raw implementation of Language.Reflection.Quotable_33ab986c : Quotable (List ConstructorDefn) Raw
PE_List a, Raw implementation of Language.Reflection.Quotable_7915b8f7 : Quotable (List (TTName, List CtorArg, Raw)) Raw
PE_List a, Raw implementation of Language.Reflection.Quotable_d09dc8b8 : Quotable (List TyConArg) Raw
PE_List a, Raw implementation of Language.Reflection.Quotable_df2fadf0 : Quotable (List ErrorReportPart) Raw
PE_List a, Raw implementation of Language.Reflection.Quotable_fc2e868 : Quotable (List String) Raw
PE_List a, TT implementation of Language.Reflection.Quotable_1507bcbc : Quotable (List CtorArg) TT
PE_List a, TT implementation of Language.Reflection.Quotable_20086ef3 : Quotable (List FunArg) TT
PE_List a, TT implementation of Language.Reflection.Quotable_33ab986c : Quotable (List ConstructorDefn) TT
PE_List a, TT implementation of Language.Reflection.Quotable_7915b8f7 : Quotable (List (TTName, List CtorArg, Raw)) TT
PE_List a, TT implementation of Language.Reflection.Quotable_d09dc8b8 : Quotable (List TyConArg) TT
PE_List a, TT implementation of Language.Reflection.Quotable_df2fadf0 : Quotable (List ErrorReportPart) TT
PE_List a, TT implementation of Language.Reflection.Quotable_fc2e868 : Quotable (List String) TT
PE_abs_85d79e7b : Integer -> Integer
PE_abs_d6648df : Int -> Int
PE_absurd_654c8984 : (h : Void) -> a
PE_absurd_9b4b794a : (h : Fin 0) -> a
PE_any_45711470 : (a -> Bool) -> List a -> Bool
PE_cast_1f219304 : (orig : Int) -> Char
PE_cast_4a482be : (orig : Nat) -> Integer
PE_cast_569d416 : (orig : Int) -> Integer
PE_cast_8c354935 : (orig : Int) -> Nat
PE_cast_a18abc1e : (orig : String) -> List Char
PE_cast_abf8387c : (orig : Integer) -> Nat
PE_cast_b8ccd99c : (orig : Char) -> Int
PE_cast_c090c40e : (orig : Integer) -> String
PE_cast_c71d3746 : (orig : Nat) -> Int
PE_cast_dd2c0e30 : (orig : String) -> Integer
PE_compare_1676ea41 : Prec -> Prec -> Ordering
PE_compare_22f242c8 : Char -> Char -> Ordering
PE_compare_32c264fb : Bool -> Bool -> Ordering
PE_compare_40cb6e4b : Integer -> Integer -> Ordering
PE_compare_6b31ad5c : Nat -> Nat -> Ordering
PE_compare_7200248c : Double -> Double -> Ordering
PE_compare_9b1b58ef : () -> () -> Ordering
PE_compare_a2d818a2 : Fin n -> Fin n -> Ordering
PE_compare_ba2f651f : Int -> Int -> Ordering
PE_compare_c1eaf49 : String -> String -> Ordering
PE_concatMap_296b1ec9 : (a -> String) -> List a -> String
PE_concatMap_8faac41f : (a -> List b) -> List a -> List b
PE_concat_2278c957 : List (List a) -> List a
PE_constructor of Prelude.Algebra.Monoid#Semigroup ty_3b7d03c1 : Semigroup (List a)
PE_constructor of Prelude.Algebra.Monoid#Semigroup ty_3b7d03e2 : Semigroup (List b)
PE_constructor of Prelude.Algebra.Monoid#Semigroup ty_fc2e868 : Semigroup String
PE_countFrom_40cb6e4b : Integer -> Integer -> Stream Integer
PE_countFrom_6b31ad5c : Nat -> Nat -> Stream Nat
PE_countFrom_ba2f651f : Int -> Int -> Stream Int
PE_decEq_32c264fb : (x1 : Bool) -> (x2 : Bool) -> Dec (x1 = x2)
PE_decEq_6b31ad5c : (x1 : Nat) -> (x2 : Nat) -> Dec (x1 = x2)
PE_decEq_6b468553 : (x1 : List String) -> (x2 : List String) -> Dec (x1 = x2)
PE_decEq_81d0650b : (x1 : (Int, Int)) -> (x2 : (Int, Int)) -> Dec (x1 = x2)
PE_decEq_88815844 : (x1 : SourceLocation) -> (x2 : SourceLocation) -> Dec (x1 = x2)
PE_decEq_ba2f651f : (x1 : Int) -> (x2 : Int) -> Dec (x1 = x2)
PE_decEq_c1eaf49 : (x1 : String) -> (x2 : String) -> Dec (x1 = x2)
PE_elemBy_3a7ca737 : Char -> List Char -> Bool
PE_elem_22f242c8 : Char -> List Char -> Bool
PE_enumFrom_85d79e7b : Integer -> Stream Integer
PE_enumFrom_abb9c3f3 : Char -> Stream Char
PE_enumFrom_d6648df : Int -> Stream Int
PE_enumFrom_dc75de74 : Nat -> Stream Nat
PE_foldl_f16fec77 : (func : acc -> elem -> acc) -> (init : acc) -> (input : List elem) -> acc
PE_foldr_4a2f4eb1 : (func : elem -> acc -> acc) -> (init : acc) -> (input : Vect n elem) -> acc
PE_foldr_940a166a : (func : elem -> acc -> acc) -> (init : acc) -> (input : Maybe elem) -> acc
PE_foldr_e148009f : (func : elem -> acc -> acc) -> (init : acc) -> (input : Binder elem) -> acc
PE_foldr_f16fec77 : (func : elem -> acc -> acc) -> (init : acc) -> (input : List elem) -> acc
PE_fromInteger_85d79e7b : Integer -> Integer
PE_fromInteger_b5e0f956 : Integer -> Double
PE_fromInteger_d6648df : Integer -> Int
PE_fromInteger_d9a4e6b4 : Integer -> Bits8
PE_fromInteger_dc75de74 : Integer -> Nat
PE_fromInteger_e3d389f : Integer -> Bits16
PE_fromInteger_e3e405d : Integer -> Bits32
PE_fromInteger_e3fee02 : Integer -> Bits64
PE_fromNat_abb9c3f3 : Nat -> Char
PE_fromNat_d6648df : Nat -> Int
PE_isInfixOf_22f242c8 : List Char -> List Char -> Bool
PE_isPrefixOf_22f242c8 : List Char -> List Char -> Bool
PE_isSuffixOfBy_3a7ca737 : List Char -> List Char -> Bool
PE_isSuffixOf_22f242c8 : List Char -> List Char -> Bool
PE_map_1a6e6d23 : (func : a -> b) -> Vect len a -> Vect len b
PE_map_622baa6c : (func : a -> b) -> IO' (MkFFI C_Types String String) a -> IO' (MkFFI C_Types String String) b
PE_map_729111da : (func : a -> b) -> Stream a -> Stream b
PE_map_b6e9086d : (func : a -> b) -> Maybe a -> Maybe b
PE_map_e3fc06f9 : (func : a -> b) -> Elab a -> Elab b
PE_map_e84935b3 : (func : a -> b) -> List a -> List b
PE_mod_40cb6e4b : Integer -> Integer -> Integer
PE_negate_85d79e7b : Integer -> Integer
PE_negate_b5e0f956 : Double -> Double
PE_negate_d6648df : Int -> Int
PE_neutral_3b7d03c1 : List a
PE_neutral_3b7d03e2 : List b
PE_neutral_fc2e868 : String
PE_pack_3b7d037f : List Char -> String
PE_pure_837faffc : a -> IO' (MkFFI C_Types String String) a
PE_pure_bd364ca1 : a -> Elab a
PE_pure_c4df80b5 : a -> IO' ffi a
PE_quote_11bb3e3a : List FunArg -> TT
PE_quote_12187275 : (List CtorArg, Raw) -> TT
PE_quote_16781088 : (TTName, List CtorArg, Raw) -> TT
PE_quote_19fbd576 : Int -> TT
PE_quote_2856ff09 : Plicity -> Raw
PE_quote_28a66304 : Bits16 -> TT
PE_quote_29340922 : List CtorArg -> TT
PE_quote_29944289 : ArithTy -> TT
PE_quote_2a782671 : List ErrorReportPart -> TT
PE_quote_394c1ea0 : CtorArg -> TT
PE_quote_39501405 : List TyConArg -> Raw
PE_quote_3ab5a8a2 : ConstructorDefn -> Raw
PE_quote_3d5619d2 : Bits16 -> Raw
PE_quote_3f121f8e : TT -> Raw
PE_quote_3f4952b0 : Plicity -> TT
PE_quote_3fd7d3f3 : ConstructorDefn -> TT
PE_quote_478eee7a : List TyConArg -> TT
PE_quote_49065bc8 : List FunArg -> Raw
PE_quote_4a689398 : List ConstructorDefn -> TT
PE_quote_4b5a3ac7 : Const -> TT
PE_quote_4cf115a8 : TTUExp -> Raw
PE_quote_4dbe8328 : Tactic -> Raw
PE_quote_4e5d6985 : Erasure -> Raw
PE_quote_4e8b4e80 : TTName -> Raw
PE_quote_4f9883b0 : List CtorArg -> Raw
PE_quote_52cd04a4 : Bits64 -> TT
PE_quote_53c658fd : NativeTy -> Raw
PE_quote_550a1776 : (List CtorArg, Raw) -> Raw
PE_quote_57b783a4 : TTName -> TT
PE_quote_591e7145 : FunArg -> Raw
PE_quote_5959da96 : Int -> Raw
PE_quote_5a6044f5 : ErrorReportPart -> Raw
PE_quote_5aa9b3b3 : TyConArg -> TT
PE_quote_5bffe9f8 : ArithTy -> Raw
PE_quote_62b348e9 : CtorArg -> Raw
PE_quote_6453dcf2 : Char -> Raw
PE_quote_66c35b6e : TT -> TT
PE_quote_683cf56a : Double -> TT
PE_quote_6bddb20e : List String -> Raw
PE_quote_6f591e81 : ErrorReportPart -> TT
PE_quote_6fbef909 : Double -> Raw
PE_quote_76b910df : Tactic -> TT
PE_quote_79604ae6 : List ErrorReportPart -> Raw
PE_quote_7a3b5c56 : Integer -> TT
PE_quote_7c189dea : IntTy -> Raw
PE_quote_7f2a32a0 : Char -> TT
PE_quote_8c122a20 : Bits8 -> TT
PE_quote_8e03b301 : Erasure -> TT
PE_quote_9339cb9c : Raw -> TT
PE_quote_93c65b63 : Bits32 -> TT
PE_quote_975e5ce5 : List ConstructorDefn -> Raw
PE_quote_a9d591dc : Universe -> TT
PE_quote_ac50ef72 : Bits64 -> Raw
PE_quote_afc38062 : TyConArg -> Raw
PE_quote_aff59616 : SourceLocation -> Raw
PE_quote_b07962c : List String -> TT
PE_quote_b684ea12 : Const -> Raw
PE_quote_b7217b5f : Nat -> Raw
PE_quote_bce2c2c1 : FunArg -> TT
PE_quote_c18a3d6a : Integer -> Raw
PE_quote_c751e1f : Bits32 -> Raw
PE_quote_d131bdb8 : NameType -> TT
PE_quote_d17d363 : SourceLocation -> TT
PE_quote_d346d368 : String -> Raw
PE_quote_d7dc3a17 : String -> TT
PE_quote_e3ac48c : Bits8 -> Raw
PE_quote_e46b23c7 : Universe -> Raw
PE_quote_e55d77da : (TTName, List CtorArg, Raw) -> Raw
PE_quote_f609a407 : Nat -> TT
PE_quote_f74ccb34 : NameType -> Raw
PE_quote_fa569582 : Raw -> Raw
PE_quote_fa93cf7e : TTUExp -> TT
PE_quote_fac8d188 : NativeTy -> TT
PE_quote_fc019d51 : IntTy -> TT
PE_quotedTy_12179418 : Raw
PE_quotedTy_1677322b : Raw
PE_quotedTy_29332ac5 : Raw
PE_quotedTy_2a297d09 : TT
PE_quotedTy_390ce668 : TT
PE_quotedTy_394b4043 : Raw
PE_quotedTy_3fd6f596 : Raw
PE_quotedTy_503bdd31 : TT
PE_quotedTy_541df23c : TT
PE_quotedTy_57b6a547 : Raw
PE_quotedTy_5aa8d556 : Raw
PE_quotedTy_5da3a65e : TT
PE_quotedTy_6f584024 : Raw
PE_quotedTy_7e0e4c3b : TT
PE_quotedTy_9338ed3f : Raw
PE_quotedTy_a4a53738 : TT
PE_quotedTy_b31ae937 : TT
PE_quotedTy_bce1e464 : Raw
PE_quotedTy_d7db5bba : Raw
PE_quotedTy_e56e5b7e : TT
PE_quotedTy_ee737a41 : TT
PE_quotedTy_f97db2b0 : TT
PE_showPrec_40cb6e4b : (d : Prec) -> (x : Integer) -> String
PE_showPrec_7200248c : (d : Prec) -> (x : Double) -> String
PE_showPrec_ba2f651f : (d : Prec) -> (x : Int) -> String
PE_show_81ff5c9 : (x : String) -> String
PE_show_85d79e7b : (x : Integer) -> String
PE_show_abb9c3f3 : (x : Char) -> String
PE_show_bfb5fb44 : (x : FileError) -> String
PE_show_d2fe2214 : (x : Bool) -> String
PE_show_d6279dd5 : (x : ()) -> String
PE_show_d6648df : (x : Int) -> String
PE_show_d9a4e6b4 : (x : Bits8) -> String
PE_show_dc75de74 : (x : Nat) -> String
PE_show_e3d389f : (x : Bits16) -> String
PE_show_e3e405d : (x : Bits32) -> String
PE_show_e3fee02 : (x : Bits64) -> String
PE_succ_85d79e7b : Integer -> Integer
PE_succ_abb9c3f3 : Char -> Char
PE_succ_d6648df : Int -> Int
PE_succ_dc75de74 : Nat -> Nat
PE_toNat_abb9c3f3 : Char -> Nat
PE_toNat_d6648df : Int -> Nat
PE_uninhabited_b38958cc : Fin 0 -> Void
PE_uninhabited_d88e9ae7 : Void -> Void
PE_with block in Decidable.Equality.Decidable.Equality.(a, b) implementation of Decidable.Equality.DecEq, method decEq_e85079e4 : (a1 : Int) -> (a' : Int) -> (warg : Dec (a1 = a')) -> (b1 : Int) -> (b' : Int) -> Dec ((a1, b1) = (a', b'))
PE_with block in Decidable.Equality.Decidable.Equality.List a implementation of Decidable.Equality.DecEq, method decEq_877d271a : (x : String) -> (xs : List String) -> (y : String) -> (warg : Dec (x = y)) -> (ys : List String) -> Dec (x :: xs = y :: ys)
PE_with block in with block in Decidable.Equality.Decidable.Equality.(a, b) implementation of Decidable.Equality.DecEq, method decEq_3386ce6a : (a1 : Int) -> (b1 : Int) -> (b' : Int) -> (warg : Dec (b1 = b')) -> Dec ((a1, b1) = (a1, b'))
PE_with block in with block in Decidable.Equality.Decidable.Equality.(a, b) implementation of Decidable.Equality.DecEq, method decEq_fcee5068 : (a1 : Int) -> (a' : Int) -> (p : (a1 = a') -> Void) -> (b1 : Int) -> (b' : Int) -> (warg : Dec (b1 = b')) -> Dec ((a1, b1) = (a', b'))
PE_with block in with block in Decidable.Equality.Decidable.Equality.List a implementation of Decidable.Equality.DecEq, method decEq_1793dbad : (x : String) -> (xs : List String) -> (y : String) -> (p : (x = y) -> Void) -> (ys : List String) -> (warg : Dec (xs = ys)) -> Dec (x :: xs = y :: ys)
PE_with block in with block in Decidable.Equality.Decidable.Equality.List a implementation of Decidable.Equality.DecEq, method decEq_a22721a1 : (x : String) -> (xs : List String) -> (ys : List String) -> (warg : Dec (xs = ys)) -> Dec (x :: xs = x :: ys)
data PrimIO : Type -> Type

Idris's primitive IO, for building abstractions on top of

Prim__IO : a -> PrimIO a
Ptr : Type
data Symbol_ : String -> Type

For 'symbol syntax. 'foo becomes Symbol_ "foo"

data Unit : Type

The canonical single-element type, also known as the trivially
true proposition.

MkUnit : ()

The trivial constructor for ().

data Void : Type

The empty type, also known as the trivially false proposition.

Use void or absurd to prove anything if you have a variable of type Void in scope.

data World : Type

A token representing the world, for use in IO

TheWorld : prim__WorldType -> World
WorldRes : Type -> Type
assert_smaller : (x : a) -> (y : b) -> b

Assert to the totality checker that y is always structurally smaller than
x (which is typically a pattern argument, and must be in normal form
for this to work)

x

the larger value (typically a pattern argument)

y

the smaller value (typically an argument to a recursive call)

assert_total : a -> a

Assert to the totality checker that the given expression will always
terminate.

assert_unreachable : a

Assert to the totality checker that the case using this expression
is unreachable

believe_me : a -> b

Subvert the type checker. This function is abstract, so it will not reduce in
the type checker. Use it with care - it can result in segfaults or worse!

call__IO : IO' ffi a -> PrimIO a
foreign : (f : FFI) -> (fname : ffi_fn f) -> (ty : Type) -> {auto fty : FTy f [] ty} -> ty

Call a foreign function.

The particular semantics of foreign function calls depend on the
Idris compiler backend in use. For the default C backend, see the
documentation for FFI_C.

For more details, please consult the Idris documentation.

f

an FFI descriptor, which is specific to the compiler backend.

fname

the name of the foreign function

ty

the Idris type for the foreign function

fty

an automatically-found proof that the Idris type works with
the FFI in question

idris_crash : (msg : String) -> a

Abort immediately with an error message

io_bind : IO' l a -> (a -> IO' l b) -> IO' l b
io_pure : a -> IO' l a
liftPrimIO : (World -> PrimIO a) -> IO' l a
mkForeignPrim : ForeignPrimType xs env t
par : Lazy a -> a
prim__addB16 : Bits16 -> Bits16 -> Bits16
prim__addB32 : Bits32 -> Bits32 -> Bits32
prim__addB64 : Bits64 -> Bits64 -> Bits64
prim__addB8 : Bits8 -> Bits8 -> Bits8
prim__addBigInt : Integer -> Integer -> Integer
prim__addChar : Char -> Char -> Char
prim__addFloat : Double -> Double -> Double
prim__addInt : Int -> Int -> Int
prim__andB16 : Bits16 -> Bits16 -> Bits16
prim__andB32 : Bits32 -> Bits32 -> Bits32
prim__andB64 : Bits64 -> Bits64 -> Bits64
prim__andB8 : Bits8 -> Bits8 -> Bits8
prim__andBigInt : Integer -> Integer -> Integer
prim__andChar : Char -> Char -> Char
prim__andInt : Int -> Int -> Int
prim__asPtr : ManagedPtr -> Ptr
prim__ashrB16 : Bits16 -> Bits16 -> Bits16
prim__ashrB32 : Bits32 -> Bits32 -> Bits32
prim__ashrB64 : Bits64 -> Bits64 -> Bits64
prim__ashrB8 : Bits8 -> Bits8 -> Bits8
prim__ashrBigInt : Integer -> Integer -> Integer
prim__ashrChar : Char -> Char -> Char
prim__ashrInt : Int -> Int -> Int
prim__believe_me : (a : Type) -> (b : Type) -> (x : a) -> b
prim__charToInt : Char -> Int
prim__complB16 : Bits16 -> Bits16
prim__complB32 : Bits32 -> Bits32
prim__complB64 : Bits64 -> Bits64
prim__complB8 : Bits8 -> Bits8
prim__complBigInt : Integer -> Integer
prim__complChar : Char -> Char
prim__complInt : Int -> Int
prim__concat : String -> String -> String
prim__divFloat : Double -> Double -> Double
prim__eqB16 : Bits16 -> Bits16 -> Int
prim__eqB32 : Bits32 -> Bits32 -> Int
prim__eqB64 : Bits64 -> Bits64 -> Int
prim__eqB8 : Bits8 -> Bits8 -> Int
prim__eqBigInt : Integer -> Integer -> Int
prim__eqChar : Char -> Char -> Int
prim__eqFloat : Double -> Double -> Int
prim__eqInt : Int -> Int -> Int
prim__eqManagedPtr : ManagedPtr -> ManagedPtr -> Int
prim__eqPtr : Ptr -> Ptr -> Int
prim__eqString : String -> String -> Int
prim__floatACos : Double -> Double
prim__floatASin : Double -> Double
prim__floatATan : Double -> Double
prim__floatATan2 : Double -> Double -> Double
prim__floatCeil : Double -> Double
prim__floatCos : Double -> Double
prim__floatExp : Double -> Double
prim__floatFloor : Double -> Double
prim__floatLog : Double -> Double
prim__floatSin : Double -> Double
prim__floatSqrt : Double -> Double
prim__floatTan : Double -> Double
prim__floatToStr : Double -> String
prim__fromFloatB16 : Double -> Bits16
prim__fromFloatB32 : Double -> Bits32
prim__fromFloatB64 : Double -> Bits64
prim__fromFloatB8 : Double -> Bits8
prim__fromFloatBigInt : Double -> Integer
prim__fromFloatChar : Double -> Char
prim__fromFloatInt : Double -> Int
prim__fromStrB16 : String -> Bits16
prim__fromStrB32 : String -> Bits32
prim__fromStrB64 : String -> Bits64
prim__fromStrB8 : String -> Bits8
prim__fromStrBigInt : String -> Integer
prim__fromStrChar : String -> Char
prim__fromStrInt : String -> Int
prim__gtB16 : Bits16 -> Bits16 -> Int
prim__gtB32 : Bits32 -> Bits32 -> Int
prim__gtB64 : Bits64 -> Bits64 -> Int
prim__gtB8 : Bits8 -> Bits8 -> Int
prim__gtBigInt : Integer -> Integer -> Int
prim__gtChar : Char -> Char -> Int
prim__gteB16 : Bits16 -> Bits16 -> Int
prim__gteB32 : Bits32 -> Bits32 -> Int
prim__gteB64 : Bits64 -> Bits64 -> Int
prim__gteB8 : Bits8 -> Bits8 -> Int
prim__gteBigInt : Integer -> Integer -> Int
prim__gteChar : Char -> Char -> Int
prim__intToChar : Int -> Char
prim__lshrB16 : Bits16 -> Bits16 -> Bits16
prim__lshrB32 : Bits32 -> Bits32 -> Bits32
prim__lshrB64 : Bits64 -> Bits64 -> Bits64
prim__lshrB8 : Bits8 -> Bits8 -> Bits8
prim__lshrBigInt : Integer -> Integer -> Integer
prim__lshrChar : Char -> Char -> Char
prim__lshrInt : Int -> Int -> Int
prim__ltB16 : Bits16 -> Bits16 -> Int
prim__ltB32 : Bits32 -> Bits32 -> Int
prim__ltB64 : Bits64 -> Bits64 -> Int
prim__ltB8 : Bits8 -> Bits8 -> Int
prim__ltBigInt : Integer -> Integer -> Int
prim__ltChar : Char -> Char -> Int
prim__ltString : String -> String -> Int
prim__lteB16 : Bits16 -> Bits16 -> Int
prim__lteB32 : Bits32 -> Bits32 -> Int
prim__lteB64 : Bits64 -> Bits64 -> Int
prim__lteB8 : Bits8 -> Bits8 -> Int
prim__lteBigInt : Integer -> Integer -> Int
prim__lteChar : Char -> Char -> Int
prim__managedNull : ManagedPtr
prim__mulB16 : Bits16 -> Bits16 -> Bits16
prim__mulB32 : Bits32 -> Bits32 -> Bits32
prim__mulB64 : Bits64 -> Bits64 -> Bits64
prim__mulB8 : Bits8 -> Bits8 -> Bits8
prim__mulBigInt : Integer -> Integer -> Integer
prim__mulChar : Char -> Char -> Char
prim__mulFloat : Double -> Double -> Double
prim__mulInt : Int -> Int -> Int
prim__negFloat : Double -> Double
prim__null : Ptr
prim__orB16 : Bits16 -> Bits16 -> Bits16
prim__orB32 : Bits32 -> Bits32 -> Bits32
prim__orB64 : Bits64 -> Bits64 -> Bits64
prim__orB8 : Bits8 -> Bits8 -> Bits8
prim__orBigInt : Integer -> Integer -> Integer
prim__orChar : Char -> Char -> Char
prim__orInt : Int -> Int -> Int
prim__peek16 : prim__WorldType -> Ptr -> Int -> Bits16
prim__peek32 : prim__WorldType -> Ptr -> Int -> Bits32
prim__peek64 : prim__WorldType -> Ptr -> Int -> Bits64
prim__peek8 : prim__WorldType -> Ptr -> Int -> Bits8
prim__peekDouble : prim__WorldType -> Ptr -> Int -> Double
prim__peekPtr : prim__WorldType -> Ptr -> Int -> Ptr
prim__peekSingle : prim__WorldType -> Ptr -> Int -> Double
prim__poke16 : prim__WorldType -> Ptr -> Int -> Bits16 -> Int
prim__poke32 : prim__WorldType -> Ptr -> Int -> Bits32 -> Int
prim__poke64 : prim__WorldType -> Ptr -> Int -> Bits64 -> Int
prim__poke8 : prim__WorldType -> Ptr -> Int -> Bits8 -> Int
prim__pokeDouble : prim__WorldType -> Ptr -> Int -> Double -> Int
prim__pokePtr : prim__WorldType -> Ptr -> Int -> Ptr -> Int
prim__pokeSingle : prim__WorldType -> Ptr -> Int -> Double -> Int
prim__ptrOffset : Ptr -> Int -> Ptr
prim__readChars : prim__WorldType -> Int -> Ptr -> String
prim__readFile : prim__WorldType -> Ptr -> String
prim__readString : prim__WorldType -> String
prim__registerPtr : Ptr -> Int -> ManagedPtr
prim__sdivB16 : Bits16 -> Bits16 -> Bits16
prim__sdivB32 : Bits32 -> Bits32 -> Bits32
prim__sdivB64 : Bits64 -> Bits64 -> Bits64
prim__sdivB8 : Bits8 -> Bits8 -> Bits8
prim__sdivBigInt : Integer -> Integer -> Integer
prim__sdivChar : Char -> Char -> Char
prim__sdivInt : Int -> Int -> Int
prim__sextB16_B32 : Bits16 -> Bits32
prim__sextB16_B64 : Bits16 -> Bits64
prim__sextB16_BigInt : Bits16 -> Integer
prim__sextB16_Int : Bits16 -> Int
prim__sextB32_B64 : Bits32 -> Bits64
prim__sextB32_BigInt : Bits32 -> Integer
prim__sextB32_Int : Bits32 -> Int
prim__sextB64_BigInt : Bits64 -> Integer
prim__sextB8_B16 : Bits8 -> Bits16
prim__sextB8_B32 : Bits8 -> Bits32
prim__sextB8_B64 : Bits8 -> Bits64
prim__sextB8_BigInt : Bits8 -> Integer
prim__sextB8_Int : Bits8 -> Int
prim__sextChar_BigInt : Char -> Integer
prim__sextInt_B16 : Int -> Bits16
prim__sextInt_B32 : Int -> Bits32
prim__sextInt_B64 : Int -> Bits64
prim__sextInt_BigInt : Int -> Integer
prim__sgtB16 : Bits16 -> Bits16 -> Int
prim__sgtB32 : Bits32 -> Bits32 -> Int
prim__sgtB64 : Bits64 -> Bits64 -> Int
prim__sgtB8 : Bits8 -> Bits8 -> Int
prim__sgtBigInt : Integer -> Integer -> Int
prim__sgtChar : Char -> Char -> Int
prim__sgtFloat : Double -> Double -> Int
prim__sgtInt : Int -> Int -> Int
prim__sgteB16 : Bits16 -> Bits16 -> Int
prim__sgteB32 : Bits32 -> Bits32 -> Int
prim__sgteB64 : Bits64 -> Bits64 -> Int
prim__sgteB8 : Bits8 -> Bits8 -> Int
prim__sgteBigInt : Integer -> Integer -> Int
prim__sgteChar : Char -> Char -> Int
prim__sgteFloat : Double -> Double -> Int
prim__sgteInt : Int -> Int -> Int
prim__shlB16 : Bits16 -> Bits16 -> Bits16
prim__shlB32 : Bits32 -> Bits32 -> Bits32
prim__shlB64 : Bits64 -> Bits64 -> Bits64
prim__shlB8 : Bits8 -> Bits8 -> Bits8
prim__shlBigInt : Integer -> Integer -> Integer
prim__shlChar : Char -> Char -> Char
prim__shlInt : Int -> Int -> Int
prim__sizeofPtr : Int
prim__sltB16 : Bits16 -> Bits16 -> Int
prim__sltB32 : Bits32 -> Bits32 -> Int
prim__sltB64 : Bits64 -> Bits64 -> Int
prim__sltB8 : Bits8 -> Bits8 -> Int
prim__sltBigInt : Integer -> Integer -> Int
prim__sltChar : Char -> Char -> Int
prim__sltFloat : Double -> Double -> Int
prim__sltInt : Int -> Int -> Int
prim__slteB16 : Bits16 -> Bits16 -> Int
prim__slteB32 : Bits32 -> Bits32 -> Int
prim__slteB64 : Bits64 -> Bits64 -> Int
prim__slteB8 : Bits8 -> Bits8 -> Int
prim__slteBigInt : Integer -> Integer -> Int
prim__slteChar : Char -> Char -> Int
prim__slteFloat : Double -> Double -> Int
prim__slteInt : Int -> Int -> Int
prim__sremB16 : Bits16 -> Bits16 -> Bits16
prim__sremB32 : Bits32 -> Bits32 -> Bits32
prim__sremB64 : Bits64 -> Bits64 -> Bits64
prim__sremB8 : Bits8 -> Bits8 -> Bits8
prim__sremBigInt : Integer -> Integer -> Integer
prim__sremChar : Char -> Char -> Char
prim__sremInt : Int -> Int -> Int
prim__stderr : Ptr
prim__stdin : Ptr
prim__stdout : Ptr
prim__strCons : Char -> String -> String
prim__strHead : String -> Char
prim__strIndex : String -> Int -> Char
prim__strRev : String -> String
prim__strSubstr : Int -> Int -> String -> String
prim__strTail : String -> String
prim__strToFloat : String -> Double
prim__subB16 : Bits16 -> Bits16 -> Bits16
prim__subB32 : Bits32 -> Bits32 -> Bits32
prim__subB64 : Bits64 -> Bits64 -> Bits64
prim__subB8 : Bits8 -> Bits8 -> Bits8
prim__subBigInt : Integer -> Integer -> Integer
prim__subChar : Char -> Char -> Char
prim__subFloat : Double -> Double -> Double
prim__subInt : Int -> Int -> Int
prim__syntactic_eq : (a : Type) -> (b : Type) -> (x : a) -> (y : b) -> Maybe (x = y)
prim__systemInfo : Int -> String
prim__toFloatB16 : Bits16 -> Double
prim__toFloatB32 : Bits32 -> Double
prim__toFloatB64 : Bits64 -> Double
prim__toFloatB8 : Bits8 -> Double
prim__toFloatBigInt : Integer -> Double
prim__toFloatChar : Char -> Double
prim__toFloatInt : Int -> Double
prim__toStrB16 : Bits16 -> String
prim__toStrB32 : Bits32 -> String
prim__toStrB64 : Bits64 -> String
prim__toStrB8 : Bits8 -> String
prim__toStrBigInt : Integer -> String
prim__toStrChar : Char -> String
prim__toStrInt : Int -> String
prim__truncB16_B8 : Bits16 -> Bits8
prim__truncB16_Int : Bits16 -> Int
prim__truncB32_B16 : Bits32 -> Bits16
prim__truncB32_B8 : Bits32 -> Bits8
prim__truncB32_Int : Bits32 -> Int
prim__truncB64_B16 : Bits64 -> Bits16
prim__truncB64_B32 : Bits64 -> Bits32
prim__truncB64_B8 : Bits64 -> Bits8
prim__truncB64_Int : Bits64 -> Int
prim__truncBigInt_B16 : Integer -> Bits16
prim__truncBigInt_B32 : Integer -> Bits32
prim__truncBigInt_B64 : Integer -> Bits64
prim__truncBigInt_B8 : Integer -> Bits8
prim__truncBigInt_Char : Integer -> Char
prim__truncBigInt_Int : Integer -> Int
prim__truncInt_B16 : Int -> Bits16
prim__truncInt_B32 : Int -> Bits32
prim__truncInt_B64 : Int -> Bits64
prim__truncInt_B8 : Int -> Bits8
prim__udivB16 : Bits16 -> Bits16 -> Bits16
prim__udivB32 : Bits32 -> Bits32 -> Bits32
prim__udivB64 : Bits64 -> Bits64 -> Bits64
prim__udivB8 : Bits8 -> Bits8 -> Bits8
prim__udivBigInt : Integer -> Integer -> Integer
prim__udivChar : Char -> Char -> Char
prim__udivInt : Int -> Int -> Int
prim__uremB16 : Bits16 -> Bits16 -> Bits16
prim__uremB32 : Bits32 -> Bits32 -> Bits32
prim__uremB64 : Bits64 -> Bits64 -> Bits64
prim__uremB8 : Bits8 -> Bits8 -> Bits8
prim__uremBigInt : Integer -> Integer -> Integer
prim__uremChar : Char -> Char -> Char
prim__uremInt : Int -> Int -> Int
prim__vm : prim__WorldType -> Ptr
prim__writeFile : prim__WorldType -> Ptr -> String -> Int
prim__writeString : prim__WorldType -> String -> Int
prim__xorB16 : Bits16 -> Bits16 -> Bits16
prim__xorB32 : Bits32 -> Bits32 -> Bits32
prim__xorB64 : Bits64 -> Bits64 -> Bits64
prim__xorB8 : Bits8 -> Bits8 -> Bits8
prim__xorBigInt : Integer -> Integer -> Integer
prim__xorChar : Char -> Char -> Char
prim__xorInt : Int -> Int -> Int
prim__zextB16_B32 : Bits16 -> Bits32
prim__zextB16_B64 : Bits16 -> Bits64
prim__zextB16_BigInt : Bits16 -> Integer
prim__zextB16_Int : Bits16 -> Int
prim__zextB32_B64 : Bits32 -> Bits64
prim__zextB32_BigInt : Bits32 -> Integer
prim__zextB32_Int : Bits32 -> Int
prim__zextB64_BigInt : Bits64 -> Integer
prim__zextB8_B16 : Bits8 -> Bits16
prim__zextB8_B32 : Bits8 -> Bits32
prim__zextB8_B64 : Bits8 -> Bits64
prim__zextB8_BigInt : Bits8 -> Integer
prim__zextB8_Int : Bits8 -> Int
prim__zextChar_BigInt : Char -> Integer
prim__zextInt_B16 : Int -> Bits16
prim__zextInt_B32 : Int -> Bits32
prim__zextInt_B64 : Int -> Bits64
prim__zextInt_BigInt : Int -> Integer
prim_fork : PrimIO () -> PrimIO Ptr
prim_fread : Ptr -> IO' l String
prim_freadChars : Int -> Ptr -> IO' l String
prim_fwrite : Ptr -> String -> IO' l Int
prim_io_bind : PrimIO a -> (a -> PrimIO b) -> PrimIO b
prim_io_pure : a -> PrimIO a
prim_lenString : String -> Int
prim_peek16 : Ptr -> Int -> IO Bits16
prim_peek32 : Ptr -> Int -> IO Bits32
prim_peek64 : Ptr -> Int -> IO Bits64
prim_peek8 : Ptr -> Int -> IO Bits8
prim_peekDouble : Ptr -> Int -> IO Double
prim_peekPtr : Ptr -> Int -> IO Ptr
prim_peekSingle : Ptr -> Int -> IO Double

Single precision floats are marshalled to Doubles

prim_poke16 : Ptr -> Int -> Bits16 -> IO Int
prim_poke32 : Ptr -> Int -> Bits32 -> IO Int
prim_poke64 : Ptr -> Int -> Bits64 -> IO Int
prim_poke8 : Ptr -> Int -> Bits8 -> IO Int
prim_pokeDouble : Ptr -> Int -> Double -> IO Int
prim_pokePtr : Ptr -> Int -> Ptr -> IO Int
prim_pokeSingle : Ptr -> Int -> Double -> IO Int

Single precision floats are marshalled to Doubles

prim_read : IO' l String
prim_write : String -> IO' l Int
really_believe_me : a -> b

Subvert the type checker. This function will reduce in the type checker.
Use it with extreme care - it can result in segfaults or worse!

replace : (x = y) -> P x -> P y

Perform substitution in a term according to some equality.

rewrite__impl : (P : a -> Type) -> (x = y) -> P y -> P x

Perform substitution in a term according to some equality.

Like replace, but with an explicit predicate, and applying the rewrite
in the other direction, which puts it in a form usable by the rewrite
tactic and term.

run__IO : IO' ffi () -> PrimIO ()
run__provider : IO a -> PrimIO a
sym : (left = right) -> right = left

Symmetry of propositional equality

trans : (a = b) -> (b = c) -> a = c

Transitivity of propositional equality

unsafePerformIO : IO' ffi a -> a
unsafePerformPrimIO : PrimIO a -> a
void : Void -> a

The eliminator for the Void type.

world : World -> prim__WorldType
(~=~) : (x : a) -> (y : b) -> Type

Explicit heterogeneous ("John Major") equality. Use this when Idris
incorrectly chooses homogeneous equality for (=).

Fixity
Non-associative, precedence 5
b

the type of the right side

a

the type of the left side

x

the left side

y

the right side